i, x:Id, k:Knd, ds:x:Id fp Type, da:a:Knd fp Type, f:(State(ds)Valtype(da;k)ds(x)?Void).
@i: with declarations 
ds:ds
da:da

effect of k(v) is x := f s v 
realizes es.
((x:Id. vartype(i;x) r ds(x)?Top)
& (e:E. (loc(e) = i  Id)  (valtype(e) r Valtype(da;kind(e))))
& (((isrcv(k))  (destination(lnk(k)) = i))  (kindtype(i;k) r Valtype(da;k))))
c (e:E.
c (loc(e) = i  Id)
c  (kind(e) = k  Knd)
c  ((timed)state after e(x) = f((state when e),val(e))  ds(x)?Top)) 

latex

Definitions

x. t(x), state@i, t  T, State(ds), S  T, x:A. B(x), , act(e), tag(e), lnk(e), es-V(es), es-M(es), acttype(e), rcvtype(e), isrcv(e), es_info(es), es-T(es), {T}, t.2, t.1, kindtype(i;k), kind(e), valtype(e), loc(e), P  Q, E, ES(the_w), vartype(i;x), P & Q, False, True, T, A, time(e), loc(e), ff, tt, outl(x), outr(x), isl(x), b, kindcase(k; a.f(a); l,t.g(l;t) ), tag(k), lnk(k), kind(e), isrcv(k), act(e), valtype(i;a), act(k), islocal(k), if b then t else f fi , w-action-dec(TA;M;i), w.TA, Action(i), doact(k;v), isnull(a), b, val(e), x(s), mk-ma, with declarations ds:dsda:daeffect of k(v) is x := f s v, M.sframe(k sends <l,tg>), M.frame(k affects x), M.ef(k,x,s,v,w), M.pre(a,s), M.init(x,v), M.da(a), M(i), M.ds(x), A c B, @i: with declarations ds:dsda:daeffect of k(v) is x := f s v, PossibleWorld(D;w), E, locl(a), rcv(l,tg), Knd, P  Q, Unit, , kind(a), SQType(T), vartype(i;x), , Valtype(da;k)

Lemmas

subtype rel self, top wf, id-deq wf, fpf-cap wf, es-vartype wf, subtype rel dep function, es-state-when wf, ma-valtype wf, es-valtype wf, es-val wf, fpf-cap-void-subtype, lnk wf, ldst wf, isrcv wf, assert wf, w-info wf, w-E wf, loc wf, eqof eq btrue, w-loc-lemma, w-isnull wf, not wf, w-action wf, w-act wf, true wf, squash wf, subtype rel wf, w-kind-lemma, w-a wf, w-kind wf, world wf, Id wf, w-valtype wf, pi2 wf, nat wf, pi1 wf, not functionality wrt iff, assert of bnot, eqff to assert, bnot wf, assert-eq-id, eqtt to assert, iff transitivity, bool wf, eq id wf, w-M wf, w-TA wf, w-action-dec wf, doact wf, false wf, actof wf, tagof wf, Id sq, w-eval wf